r:. ((r = 0  ))  ((1/r * r) = 1  ) 

latex

Definitions	, P & Q, t  T, P  Q, P  Q, P  Q, x:A. B(x), S  T
Lemmas	qmul inv, assert-qeq, qeq wf2, assert wf, not functionality wrt iff, rationals wf, not wf, int inc rationals, qinv wf, qmul com